Skip to content

feat(CategoryTheory): composition of profunctors#38086

Open
dagurtomas wants to merge 45 commits into
leanprover-community:masterfrom
dagurtomas:profunctor-comp
Open

feat(CategoryTheory): composition of profunctors#38086
dagurtomas wants to merge 45 commits into
leanprover-community:masterfrom
dagurtomas:profunctor-comp

Conversation

@dagurtomas

@dagurtomas dagurtomas commented Apr 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas added the WIP Work in progress label Apr 15, 2026
@github-actions

github-actions Bot commented Apr 15, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 42cfb88564

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Profunctor.Comp (new file) 468

Declarations diff (regex)

+ associator
+ associatorComponents
+ comp
+ compDiagram
+ compDiagramMap
+ compDiagramMap_comp
+ compDiagramMap_id
+ comp_whiskerLeft
+ comp_whiskerRight
+ id_whiskerLeft
+ id_whiskerRight
+ leftUnitor
+ rightUnitor
+ univComp
+ whiskerLeft
+ whiskerLeft_comp
+ whiskerLeft_id
+ whiskerRight
+ whiskerRight_comp
+ whiskerRight_id
+ whisker_assoc
+ whisker_exchange

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 42cfb88).

  • +42 new declarations
  • −0 removed declarations
+CategoryTheory.Profunctor.associator
+CategoryTheory.Profunctor.associatorComponents
+CategoryTheory.Profunctor.associatorComponents_hom
+CategoryTheory.Profunctor.associatorComponents_inv
+CategoryTheory.Profunctor.associator_hom_app_app
+CategoryTheory.Profunctor.associator_inv_app_app
+CategoryTheory.Profunctor.comp
+CategoryTheory.Profunctor.compDiagram
+CategoryTheory.Profunctor.compDiagramMap
+CategoryTheory.Profunctor.compDiagramMap_app_app
+CategoryTheory.Profunctor.compDiagramMap_comp
+CategoryTheory.Profunctor.compDiagramMap_id
+CategoryTheory.Profunctor.compDiagram_map_app
+CategoryTheory.Profunctor.compDiagram_obj_map
+CategoryTheory.Profunctor.compDiagram_obj_obj
+CategoryTheory.Profunctor.comp_map_app
+CategoryTheory.Profunctor.comp_obj_map
+CategoryTheory.Profunctor.comp_obj_obj
+CategoryTheory.Profunctor.comp_whiskerLeft
+CategoryTheory.Profunctor.comp_whiskerRight
+CategoryTheory.Profunctor.id_whiskerLeft
+CategoryTheory.Profunctor.id_whiskerRight
+CategoryTheory.Profunctor.leftUnitor
+CategoryTheory.Profunctor.leftUnitor_hom_app_app
+CategoryTheory.Profunctor.leftUnitor_inv_app_app
+CategoryTheory.Profunctor.rightUnitor
+CategoryTheory.Profunctor.rightUnitor_hom_app_app
+CategoryTheory.Profunctor.rightUnitor_inv_app_app
+CategoryTheory.Profunctor.univComp
+CategoryTheory.Profunctor.univComp_map_app
+CategoryTheory.Profunctor.univComp_obj_map
+CategoryTheory.Profunctor.univComp_obj_obj
+CategoryTheory.Profunctor.whiskerLeft
+CategoryTheory.Profunctor.whiskerLeft_app_app
+CategoryTheory.Profunctor.whiskerLeft_comp
+CategoryTheory.Profunctor.whiskerLeft_id
+CategoryTheory.Profunctor.whiskerRight
+CategoryTheory.Profunctor.whiskerRight_app_app
+CategoryTheory.Profunctor.whiskerRight_comp
+CategoryTheory.Profunctor.whiskerRight_id
+CategoryTheory.Profunctor.whisker_assoc
+CategoryTheory.Profunctor.whisker_exchange
Increase in strong tech debt: (relative, absolute) = (8.56, 0.00)
Current number Change Type (strong)
4538 9 backward.defeqAttrib.useBackward
5690 8 backward.isDefEq.respectTransparency
Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
Current number Change Type (weak)
4997 1 exposed public sections

Current commit 42cfb88564
Reference commit 50b02783d6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions Bot added the t-category-theory Category theory label Apr 15, 2026
@mathlib-dependent-issues mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 15, 2026
@dagurtomas dagurtomas mentioned this pull request Apr 17, 2026
Closed
robin-carlier
robin-carlier reviewed May 18, 2026
View reviewed changes
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated

set_option backward.isDefEq.respectTransparency false in
attribute [local simp] Types.chosenCoend_def chosenCoend.map_apply in
lemma associatorComponents_aux₁ {X : C} {Y : Fᵒᵖ} {e e' : E} {d d' : D}

@robin-carlier robin-carlier May 18, 2026

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a way to spin things so that this one (and the one below) is private?
(I can get that to work by replacing the exact associatorComponents_aux₁ _ _ _ h₁ with exact (by exact associatorComponents_aux₁ _ _ _ h₁) in the def of associator component, but this is quite ugly.

@dagurtomas dagurtomas May 20, 2026

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

exact by exact feels like a hack (why doesn't it just do the same thing as exact?). But I agree these should ideally be private. I don't know a good solution

Comment thread Mathlib/CategoryTheory/Profunctor/Bicategory.lean Outdated
Comment thread Mathlib/CategoryTheory/Profunctor/Bicategory.lean Outdated
Comment thread Mathlib/CategoryTheory/Profunctor/Bicategory.lean Outdated
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated
Comment thread Mathlib/CategoryTheory/Profunctor/Bicategory.lean Outdated
Comment thread Mathlib/CategoryTheory/Profunctor/Bicategory.lean Outdated
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label May 18, 2026
dagurtomas and others added 3 commits May 20, 2026 09:21
@dagurtomas @robin-carlier
Apply suggestions from code review
33e3bbf 
Co-authored-by: Robin Carlier <57142648+robin-carlier@users.noreply.github.com>
@dagurtomas
chore: remove profunctor bicategory from PR
d650f12
@dagurtomas
chore: remove stale comment
d3ae39b
@dagurtomas dagurtomas mentioned this pull request May 20, 2026
Open
1 task
@dagurtomas

dagurtomas commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

Moved the bicategory to a followup PR: #39619

@dagurtomas dagurtomas removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 20, 2026
adamtopaz
adamtopaz reviewed May 27, 2026
View reviewed changes
Comment thread Mathlib/Logic/Relation.lean Outdated
@adamtopaz

adamtopaz commented May 27, 2026

Copy link
Copy Markdown
Contributor

Please make sure to update the "future work" section in the docs of Profunctor/Basic.lean.

adamtopaz
adamtopaz reviewed May 27, 2026
View reviewed changes
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated
adamtopaz
adamtopaz reviewed May 27, 2026
View reviewed changes
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated
adamtopaz
adamtopaz reviewed May 27, 2026
View reviewed changes
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated
dagurtomas
dagurtomas commented Jun 14, 2026
View reviewed changes
Comment thread Mathlib/Logic/Relation.lean Outdated
dagurtomas
dagurtomas commented Jun 14, 2026
View reviewed changes
Comment thread Mathlib/Logic/Relation.lean Outdated
@mathlib-splicebot mathlib-splicebot Bot mentioned this pull request Jun 14, 2026
Closed
dagurtomas
dagurtomas commented Jul 2, 2026
View reviewed changes
Comment thread Mathlib/CategoryTheory/Profunctor/Comp.lean Outdated
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@adamtopaz adamtopaz adamtopaz left review comments
@robin-carlier robin-carlier robin-carlier left review comments
+1 more reviewer
@mathlib-splicebot mathlib-splicebot[bot] mathlib-splicebot[bot] left review comments
Reviewers whose approvals may not affect merge requirements

Assignees

@robin-carlier robin-carlier

Labels

t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@dagurtomas @adamtopaz @robin-carlier @adrianmartir